ds:fpf(Id; x.Type), da:fpf(Knd; k.Type), A:ecl-trans-tuple{i:l}
ds:fpf(Id; x.Type), da:fpf(Knd; k.Type), A:ecl-trans-tuple(ds; da).
ecl-trans-act(ds; da; A)  (event-info(ds;da) List)prop{i:l} 

latex

Definitions	t  T, ma-valtype(da; k), P  Q, False, A, A  B, , x:A. B(x), ecl-trans-state(v; L), ecl-trans-ks(v), Knd, (x  l), ecl-trans-a(v), b, prop{i:l}, A c B, event-info(ds;da), spreadn(a; x,y,z.t(x;y;z)), append(as; bs), P  Q, x:A. B(x), ecl-trans-act(ds; da; A), Id, x. t(x), fpf(A; a.B(a)), ecl-trans-tuple{i:l}(ds; da)
Lemmas	ecl-trans-tuple wf, fpf wf, Id wf, append wf, event-info wf, nat wf, assert wf, ecl-trans-a wf, l member wf, Knd wf, ecl-trans-ks wf, ecl-trans-state wf